open util/integer as integer
//Per semplicità, i costi monetari sono trattati come Int e non come FLoat

///////////////////////////////////////////////////////////////////////////////////////////////////////////////
//#HELPER SIGNATURES
///////////////////////////////////////////////////////////////////////////////////////////////////////////////


sig DateTime {
	timestamp : Int //Data per semplicità trattata mediante unix timestamp
} {
	//Vengono accettate solo date successive al 1/1/2013
	timestamp >= 1356998400
}

sig Price {
	amount : Int
} {
	amount >= 0
}

//Periodo è riferido ai periodi dell'anno di default in cui vengono categorizzati i pacchetti, NON ad un generico periodo data_inizio - data_fine
sig Periodo {
	start : one DateTime,
	end : one DateTime
}


///////////////////////////////////////////////////////////////////////////////////////////////////////////////
//#MAIN SIGNATURES
///////////////////////////////////////////////////////////////////////////////////////////////////////////////


sig UtenteEsterno, Username, Password, Camera {}
//Le precedenti signature vengono usate come primitive vuote, in quanto i loro attributi sono ininfluenti rispetto alle finalità della nostra
//modellazione in alloy. Non sono stati inseriti per semplicità tutti gli attributi testuali su cui sono semplicemente necessari controlli sulla 
//lunghezza delle stringhe

abstract sig Account {
	username : one Username,
	password : one Password
}

sig Impiegato extends Account {
	
}

sig Utente extends Account {

}

sig Aeroporto {
	location : one Localita
}

sig Volo {
	departure : one Aeroporto,
	destination : one Aeroporto,
	dateTime : one DateTime,
	price : one Price,
	availability : one Int
} {
	availability >= 0
}

sig Nazione {
	locations : some Localita
}

sig Localita {
	nation : one Nazione,
	hotel : set Hotel,
	excursion : set Escursione,
	package : set Pacchetto,
	airport : set Aeroporto
}

sig Hotel {
	location : one Localita,
	availability : set Disponibilita
}

sig Disponibilita {
	room : one Camera,
	from : DateTime,
	to : DateTime,
	remaining : one Int,
	price : one Price
} {
	remaining >= 0
}

sig Escursione {
	location : one Localita,
	dateTime : one DateTime,
	price : one Price
}

sig Pacchetto {
	location : one Localita,
	period : one Periodo,
	flight : some Volo,
    defaultHotel : one Hotel,
	alternativeHotel : set Hotel,
	defaultExcursion : one Escursione,
	alternativeExcursion : set Escursione
} {

	//Intersezione vuota tra prodotti di default e alternativi
	no (defaultHotel & alternativeHotel)
	no (defaultExcursion & alternativeExcursion)

	//Gli hotel devono trovarsi nella stessa località del pacchetto
	all h : hotels[this] | h.location = location

	//Voli hanno destinazione coerente con località e periodo coerente con il pacchetto
	all f : flight |  (f.destination.location = location || f.departure.location = location) && inPeriod[f.dateTime, period]

	//Le escursioni devono essere organizzate per quel periodo
	all e : excursions[this] | e.location = location && inPeriod[e.dateTime, period]

	//Gli hotel devono avere disponibilità di camere per quel periodo
	all h : hotels[this] | some d : h.availability | d.remaining > 0 && (inPeriod[d.from, period] || inPeriod[d.to, period])
}

sig Prenotazione {
	user : one Utente,
	originalPackage : one Pacchetto,
	chosenHotel : one Hotel,
	chosenDays : set Disponibilita,
	chosenExcursion : one Escursione,
	finalPrice : Price
}


///////////////////////////////////////////////////////////////////////////////////////////////////////////////
//#FUNCTIONS
///////////////////////////////////////////////////////////////////////////////////////////////////////////////


//Restituisce l'insieme di tutti gli hotel associati ad un pacchetto
fun hotels [p : Pacchetto] : some Hotel {
	p.(defaultHotel + alternativeHotel)
}

//Restituisce l'insieme di tutte le escursioni associate ad un pacchetto
fun excursions [p : Pacchetto] : some Escursione {
	p.(defaultExcursion + alternativeExcursion)
}


///////////////////////////////////////////////////////////////////////////////////////////////////////////////
//#HELPER PREDICATES
///////////////////////////////////////////////////////////////////////////////////////////////////////////////


//Controlla che una data rientri in un particolare periodo
pred inPeriod [d : DateTime, p : Periodo] {
	d.timestamp <= p.end.timestamp && d.timestamp >= p.start.timestamp
}

//Login
pred loginA [ue : UtenteEsterno, usr : Username, pwd : Password] {
	one u : Utente | u.username = usr && u.password = pwd
}


///////////////////////////////////////////////////////////////////////////////////////////////////////////////
//#FACTS
///////////////////////////////////////////////////////////////////////////////////////////////////////////////


//Simmetria delle relazioni tra Località e Hotel, Escursione, Pacchetto
fact simmetricRelations {
	all l : Localita, h : Hotel | l = h.location <=> h in l.hotel
	all l : Localita, e : Escursione | l = e.location <=> e in l.excursion
	all l : Localita, p : Pacchetto | l = p.location <=> p in l.package
	all l : Localita, n : Nazione | l in n.locations <=> n = l.nation
	all l : Localita, a : Aeroporto | a in l.airport <=> l = a.location
}

//Non devono esistere due account con lo stesso Username
fact noDoubleAccount {
	no disj a,b : Account |  a.username = b.username
}

//Non ci devono essere pacchetti viaggio con stessa destinazione, periodo e hotel
fact noDoublePackage {
	no disj a,b : Pacchetto |  a.location = b.location && a.period = b.period && no (hotels[a] & hotels[b]) 
}

//Periodi default dell'anno: durano almeno un giorno, non esistono duplicati, end > start
fact coherentPeriods {
	all p : Periodo | p.end.timestamp >= (p.start.timestamp + 86400)  //60*60*24
	no disj a,b : Periodo | a.start.timestamp = b.start.timestamp && a.end.timestamp = b.end.timestamp
	//Per ora non si considerano le sovrapposizioni dei periodi, ma successivamente verranno aggiunte altre restrizioni
}

///////////////////////////////////////////////////////////////////////////////////////////////////////////////
//#ASSERTIONS
///////////////////////////////////////////////////////////////////////////////////////////////////////////////


//Verifica che i voli di un pacchetto abbiano stessa destinazione e periodo del pacchetto
assert coherentFlights {
	all p : Pacchetto | all f : p.flight | (f.destination.location = p.location || f.departure.location = p.location) && inPeriod[f.dateTime, p.period]
}

check  coherentFlights

//Controllo di coerenza sulle escursioni di un pacchetto
assert coherentExcursions {
	all p : Pacchetto | all e : excursions[p] | e.location = p.location && inPeriod[e.dateTime, p.period]
}

check coherentExcursions

//Verifica che gli hotel di un pacchetto abbiano stessa località del pacchetto
assert coherentHotels {
	all p : Pacchetto | all h : hotels[p] | h.location = p.location
}

check coherentHotels


//Verifica che, per ogni pacchetto, l'hotel di default non faccia parte degli hotel alternativi
assert noDuplicateHotels {
	all p : Pacchetto | no (p.defaultHotel & p.alternativeHotel)
}

check noDuplicateHotels

//Verifica che, per ogni pacchetto, l'escursione di default non faccia parte delle escursioni alternative
assert noDuplicateExcursions {
	all p: Pacchetto | no (p.defaultExcursion & p.alternativeExcursion)
}

check  noDuplicateExcursions

//Non ci devono essere account uguali
assert noDoubleAccount {
	no disj a,b : Pacchetto |  a.location = b.location && a.period = b.period && no (hotels[a] & hotels[b]) 
}

check noDoubleAccount

//Non ci devono essere pacchetti viaggio con stessa destinazione, periodo e hotel
assert noDoublePackage {
	no disj a,b : Pacchetto |  a.location = b.location && a.period = b.period && no (hotels[a] & hotels[b]) 
}

check noDoublePackage

//Coerenza nella località dei prodotti base
assert simmetricRelations {
	all l : Localita, h : Hotel | l = h.location <=> h in l.hotel
	all l : Localita, e : Escursione | l = e.location <=> e in l.excursion
	all l : Localita, p : Pacchetto | l = p.location <=> p in l.package
	all l : Localita, n : Nazione | l in n.locations <=> n = l.nation
	all l : Localita, a : Aeroporto | a in l.airport <=> l = a.location
}

check simmetricRelations

//Controllo coerenza periodi
assert coherentPeriods {
	all p : Periodo | p.end.timestamp >= (p.start.timestamp + 86400)
	no disj a,b : Periodo | a.start.timestamp = b.start.timestamp && a.end.timestamp = b.end.timestamp
	//Per ora non si considerano le sovrapposizioni dei periodi, ma successivamente verranno aggiunte altre restrizioni
}

check coherentPeriods

//Controllo prezzi
assert coherentPrices {
	all e : Escursione | e.price.amount >= 0
	all f : Volo | f.price.amount >= 0
	all d : Disponibilita | d.price.amount >= 0
}

check coherentPrices

//Disponibilità degli hotel nei pacchetti
assert hotelAvailability {
	all p : Pacchetto | all h : hotels[p] | some d : h.availability | d.remaining > 0 && (inPeriod[d.from, p.period] || inPeriod[d.to, p.period])
}

check hotelAvailability


///////////////////////////////////////////////////////////////////////////////////////////////////////////////
//#SHOW
///////////////////////////////////////////////////////////////////////////////////////////////////////////////


pred show () {
	#Pacchetto = 1
	#Hotel = 2
	#Escursione = 2
	#Volo = 3
}
run show


///////////////////////////////////////////////////////////////////////////////////////////////////////////////
//#FUNCTIONAL PREDICATES & DATABASE SIGNATURE
///////////////////////////////////////////////////////////////////////////////////////////////////////////////

//Vengono di seguito elencati a titolo indicativo alcuni predicati che rappresentano
//operazioni ricorrenti nel sistema

//La sig Database serve solo per chiarire meglio la funzione di alcuni predicati
sig Database {
	allPackages : set Pacchetto,
	allFlights : set Volo,
	allHotels : set Hotel,
	reservations : set Prenotazione		
	//Altri elementi non inseriti per semplicità.
} {
	#Database = 1
	all p : Pacchetto | p in allPackages
	all f : Volo | f in allFlights
	all h : Hotel | h in allHotels
	all r : Prenotazione | r in reservations
}

//Verranno inseriti qui solo alcuni esempi a scopo dimostrativo delle operazioni che potranno essere svolte dal sistema
//In generale, l'eliminazione di contenuti

//Aggiungi pacchetto
pred addPackage [d : Database, i : Impiegato, p : Pacchetto] {
	!(p in d.allPackages) implies	d.allPackages = d.allPackages + p
}

run addPackage

//Elimina volo dal database solo se non è già assegnato ad un pacchetto
pred deleteFlight [d : Database, i : Impiegato, f : Volo] {
	(f in d.allFlights && no p : Pacchetto | f in p.flight) implies d.allFlights = d.allFlights - f
}

run deleteFlight

//Prenotazione
pred reservePackage [d : Database, u : Utente, r : Prenotazione, p : Pacchetto, h : Hotel, a : set Disponibilita] {
	r.originalPackage = p
	r.chosenHotel = h
	r.chosenDays = a
	(p in d.allPackages && h in d.allHotels && h in hotels[p]) implies d.reservations = d.reservations + r
} 

run reservePackage
